b:. b | 1  b =  1 

latex

Definitions	x:A. B(x), , P  Q, b | a, t  T, AB, A, False, , Dec(P), P  Q, i =  j, Prop, P  Q, P & Q
Lemmas	divides invar 1, le wf, decidable le, zero divs only zero, decidable int equal, divisors bound, divides wf, nat wf